Sequential machines present unique problems to providing reliable designs. Often original sequential machine is reimplemented in a new fabrication technology or reimplemented within a given fabrication technology, In practice, the new sequential design must be checked against the original, whether the new design is implemented by hand or through the use of a synthesis tool. This area of comparison is referred to as "design verification". Present design verification techniques are inadequate to check for functional equivalence, since they utilize a partial simulation of the sequential behavior of a new design by itself or in its intended environment.
Synchronous designs generally are modeled at the gate level in terms of combinational elements and Primitive Storage Elements (PSEs). APSE is a device that shifts its input to its output on a clock event and holds its value until the next clock event. An example of a primitive storage element is a simple D-flip-flop (without enable or reset). Most real storage devices, such as D-flip-flops with an enable, reset, and both Q and Q outputs. can be modeled as a network of these primitive storage elements together with combinational logic. However, one of the limiting factors of all state machines utilized in, for example digital computers, is the length of time required for signals to propagate through all of the logic gates between PSEs. Therefore, an original design is often modified to shorten the length of the signal propagation time.
There are three important areas in design verification. These are formal verification, synthesis, and Automatic Test Pattern Generation (ATPG), With respect to ATPG, a machine is designed so that when the machine is actually fabricated, it can be tested to determine whether the fabricated system is equivalent to a flawlessly fabricated design. With respect to synthesis, design verification is required to show that a resynthesized design is equivalent to an original design or that a synthesized design conforms to its specification. In synthesizing a design, a designer can provide the storage elements and logic equations relating storage elements to each other and to the inputs and outputs of the design. Then a synthesis machine is allowed to generate a design from this information. The third, formal verification, allows a designer to determine not only if his design is equivalent to another known design, but also if his design is equivalent to itself.